$\forall$$A$, $B$:es\_realizer\{i:l\}. R{-}compat\{i:l\}($A$; $B$) $\in$ Prop$_{\mbox{\scriptsize i'}}$